le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
↳ QTRS
↳ DependencyPairsProof
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
IF(false, x, b, y, z) → LOOP(x, b, times(b, y), s(z))
LOOP(x, s(s(b)), s(y), z) → IF(le(x, s(y)), x, s(s(b)), s(y), z)
TIMES(s(x), y) → PLUS(y, times(x, y))
LOOP(x, s(s(b)), s(y), z) → LE(x, s(y))
TIMES(s(x), y) → TIMES(x, y)
LOG(s(x), s(s(b))) → LOOP(s(x), s(s(b)), s(0), 0)
IF(false, x, b, y, z) → TIMES(b, y)
LE(s(x), s(y)) → LE(x, y)
PLUS(s(x), y) → PLUS(x, y)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IF(false, x, b, y, z) → LOOP(x, b, times(b, y), s(z))
LOOP(x, s(s(b)), s(y), z) → IF(le(x, s(y)), x, s(s(b)), s(y), z)
TIMES(s(x), y) → PLUS(y, times(x, y))
LOOP(x, s(s(b)), s(y), z) → LE(x, s(y))
TIMES(s(x), y) → TIMES(x, y)
LOG(s(x), s(s(b))) → LOOP(s(x), s(s(b)), s(0), 0)
IF(false, x, b, y, z) → TIMES(b, y)
LE(s(x), s(y)) → LE(x, y)
PLUS(s(x), y) → PLUS(x, y)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
PLUS(s(x), y) → PLUS(x, y)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(s(x), y) → PLUS(x, y)
The value of delta used in the strict ordering is 1/2.
POL(PLUS(x1, x2)) = (2)x_1
POL(s(x1)) = 1/4 + (7/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
TIMES(s(x), y) → TIMES(x, y)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMES(s(x), y) → TIMES(x, y)
The value of delta used in the strict ordering is 1/2.
POL(TIMES(x1, x2)) = (2)x_1
POL(s(x1)) = 1/4 + (7/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
LE(s(x), s(y)) → LE(x, y)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LE(s(x), s(y)) → LE(x, y)
The value of delta used in the strict ordering is 15/8.
POL(s(x1)) = 1/2 + (13/4)x_1
POL(LE(x1, x2)) = (15/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
IF(false, x, b, y, z) → LOOP(x, b, times(b, y), s(z))
LOOP(x, s(s(b)), s(y), z) → IF(le(x, s(y)), x, s(s(b)), s(y), z)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))